O que é Programação Funcional
Cálculo λ
e = λx.e -- abstração
| e e -- aplicação
| x -- váriaveis
- α-equivalência: renomear variáveis ligadas
- β-redução: substituir variáveis ligadas por expressões em aplicações
- η-conversão: noção de extensionalidade
- Independente da escolha de avaliação
Estruturas de Dados Algébricas
data List a = Empty
| Cons a (List a)
xs_0 = Empty
xs_1 = Cons 1 Empty
xs_2 = Cons 1 (Cons 2 Empty)
xs_0 = []
xs_1 = [1]
xs_2 = [1,2]
Estruturas de Dados Algébricas
sum [1,2,3] = 6
sum Empty = 0
sum (Cons x xs) = x + sum xs
sum (Cons 1 (Cons 2 (Cons 3 Empty)))
= 1 + sum (Cons 2 (Cons 3 Empty))
sum (Cons 2 (Cons 3 Empty))
= 2 + sum (Cons 3 Empty)
sum (Cons 3 Empty)
= 3 + sum Empty
sum Empty
= 0
= 3 + 0
= 2 + 3 + 0
= 1 + 2 + 3 + 0
= (+) 1 ((+) 2 ((+) 3 0))
Estruturas de Dados Algébricas
sum Empty = 0
sum (Cons x xs) = x + sum xs
sum xs = foldr (+) 0 xs
foldr c e Empty = e
foldr c e (Cons x xs) = c x (foldr c e xs)
foldr c e Empty = e
foldr c e (Cons x xs) = c x (foldr c e xs)
foldr c e xs = loop xs
where loop Empty = e
loop (Cons x xs) = c x (loop xs)
Estruturas de Dados Algébricas
sum = foldr (+) 0
product = foldr (*) 1
any = foldr (||) False
all = foldr (&&) True
foldr (+) 0 (Cons 1 (Cons 2 (Cons 3 Empty)))
= (+) 1 ((+) 2 ((+) 3 0))
foldr (*) 1 (Cons 1 (Cons 2 (Cons 3 Empty)))
= (*) 1 ((*) 2 ((*) 3 1))
Estruturas de Dados Algébricas
as = Cons 1 (Cons 2 Empty)
bs = Cons 3 (Cons 4 Empty)
abs = Cons 1 (Cons 2 (Cons 3 (Cons 4 Empty)))
foldr c e (Cons 1 (Cons 2 Empty))
= c 1 (c 2 e))
foldr Cons (Cons 3 (Cons 4 Empty)) (Cons 1 (Cons 2 Empty))
= Cons 1 (Cons 2 (Cons 3 (Cons 4 Empty)))
append as bs = foldr Cons bs as
Avaliação não Ansiosa (inclui Preguiçosa)
head (Cons x _) = x
last (Cons x Empty) = x
last (Cons x xs) = last xs
take 0 _ = Empty
take _ Empty = Empty
take n (Cons x xs) = Cons x (take (n-1) xs)
Avaliação não Ansiosa (inclui Preguiçosa)
fibs = Cons 0 (Cons 1 (more fibs))
where more (Cons x xs) = Cons (x + head xs) (more xs)
fibs = Cons 0 (Cons 1 ?0)
last (take 4 fibs)
= last (take 4 (Cons 0 (Cons 1 ?0)))
= last (Cons 0 (take (4-1) (Cons 1 ?0)))
= last (Cons 0 (take 3 (Cons 1 ?0)))
= last (Cons 0 (Cons 1 (take (3-1) ?0)))
= last (Cons 1 (take (3-1) ?0))
= last (Cons 1 (take 2 ?0))
= last (Cons 1 (take 2 (Cons (0 + head (Cons 1 ?0)) (more (Cons 1 ?0)))))
fibs = Cons 0 (Cons 1 (Cons (0 + head (Cons 1 ?0)) (more (Cons 1 ?0))))
= last (Cons 1 (Cons (0 + head (Cons 1 ?0)) (take (2-1) (more (Cons 1 ?0)))))
= last (Cons (0 + head (Cons 1 ?0)) (take (2-1) (more (Cons 1 ?0))))
= last (Cons (0 + head (Cons 1 ?0)) (take 1 (more (Cons 1 ?0))))
= last (Cons (0 + head (Cons 1 ?0)) (take 1 (Cons (1 + head ?0) (more ?0))))
= last (Cons (0 + head (Cons 1 ?0)) (Cons (1 + head ?0) (take (1-1) (more ?0))))
= last (Cons (1 + head ?0) (take (1-1) (more ?0)))
= last (Cons (1 + head ?0) (take 0 (more ?0)))
= last (Cons (1 + head ?0) Empty)
= 1 + head ?0
= 1 + head (Cons (0 + head (Cons 1 ?0)) (more (Cons 1 ?0)))
= 1 + (0 + head (Cons 1 ?0))
= 1 + (0 + 1)
= 1 + 1
fibs = Cons 0 (Cons 1 (Cons 1 ?1))
= 2
Avaliação não Ansiosa (inclui Preguiçosa)
length Empty = 0
length (Cons _ xs) = 1 + length xs
prop xs = length xs > 5
prop fibs == ⊥ -- recursão infinita :(
prop' (Cons _ (Cons _ (Cons _ (Cons _ (Cons _ (Cons _ _)))))) = True
prop' _ = False
prop' fibs == True -- mas temos que reescrever o código :/
Avaliação não Ansiosa (inclui Preguiçosa)
data N = Z -- A natural N is either zero (Z)
| S N -- or the sucessor of a natural (S N)
instance Ord N where
Z <= _ = True
_ <= Z = False
(S x) <= (S y) = x <= y
Avaliação não Ansiosa (inclui Preguiçosa)
prop'' xs = genericLength xs > (5 :: N)
prop'' fibs == True -- =D
prop''' xs = case (genericLength xs :: N) of
(S (S (S (S (S (S _)))))) = True
_ = False
prop' (Cons _ (Cons _ (Cons _ (Cons _ (Cons _ (Cons _ _)))))) = True
prop' _ = False